(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix Multiplication *)
Require Import List.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.list_function.
Require Import Matrix.Mat.Mat_IO.
Require Import Matrix.Mat.Mat_map.
Require Import Matrix.Mat.Mat_trans.

Import ListNotations.

Section Mul.
Variable A:Set.
Variable Zero:A.
Variable One:A.
Variable add:A->A->A.
Variable mul:A->A->A.

(* ################################################################# *)
(** * Definition of Multiplication Function between Matrices *)

Section Mul_def.

(** ** The Multiplication of List and Two-dimensional List *)

(** *** l_mul_dl *)
(** The multiplication of list and two-dimensional list. *)
Fixpoint l_mul_dl (l:list A) (m:list(list A)) :=
  match m with
  | nil => nil
  | a :: t 
    => product' A Zero add mul l a :: l_mul_dl l t
  end.

(** *** dl_mul_dl *)
(** The multiplication of two-dimensional lists. *)
Fixpoint dl_mul_dl (left right:list(list A)) :=
  match left with
  | nil => nil
  | a :: t => l_mul_dl a right 
  :: dl_mul_dl t right
  end.

(** *** mat_mul_mat *)
(** The multiplication of matrices returns a two-dimensional list. *)
Definition mat_mul_mat {m n p:nat} (left:@Mat A m n ) (right:@Mat A n p):=
  let l1 := mat A m n left in
  let right' := trans A Zero right in
  let l2 := mat A p n right' in
    dl_mul_dl l1 l2.

(** ** Properties of the Functions above   **)

(** *** length_l_mul_dl *)
(** The length of the list obtained by multiplying the list l and the
    two-dimensional list ma is equal to the height of ma. *)
Lemma length_l_mul_dl : forall (l:list A) (ma:list (list A)), 
  length(l_mul_dl l ma) = height ma.
Proof.
  intros l.
  induction ma.
  - simpl. auto.
  - simpl. rewrite IHma. auto.
Qed.

(** *** width_dl_mul_dl_nilr *)
(** The width of the two-dimensional list obtained by the 
    multiplication of a two-dimensional list and nil is equal to 0. *)
Lemma width_dl_mul_dl_nilr: forall left , 
  width (dl_mul_dl left nil) 0.
Proof.
  induction left.
  - simpl. auto.
  - simpl. split. auto. auto.
Qed.

(** *** height_dl_mul_dl *)
(** The height of the two-dimensional list obtained by the 
    multiplication of two-dimensional lists is equal to the height of
    the two-dimensional lists. *)
Lemma height_dl_mul_dl : forall (left right:list(list A)),
   height (dl_mul_dl left right) = height left.
Proof.
  induction left.
  - simpl. auto.
  - simpl. intros. rewrite IHleft. auto.
Qed.

(** *** width_dl_mul_dl *)
(** The width of the two-dimensional list obtained by the 
    multiplication of two-dimensional lists is equal to the width of
    the two-dimensional lists. *)
Lemma width_dl_mul_dl : forall (n:nat) (left right:list(list A)),
  height right = n  -> width  (dl_mul_dl left right) n.
Proof.
  induction n.
  induction left.
  induction right.
  - simpl. auto.
  - simpl. intros. inversion H.
  - simpl. intros. split. rewrite length_l_mul_dl. auto. apply IHleft. auto. 
  - induction left. induction right.
    + simpl. auto.
    + simpl. auto.
    + induction right.
      { simpl. intros. split. auto. inversion H. }
      { simpl. intros. split. rewrite length_l_mul_dl. 
      auto. apply IHleft. auto. }
Qed.

(** *** height_mat_mul_mat *)
(** The height of the two-dimensional list obtained by the 
    multiplication of matrices is equal to the height of the matrices. *)
Lemma height_mat_mul_mat : forall {m n p:nat} (left:@Mat A m n)
  (right :@Mat A n p),
  height (mat_mul_mat left right) = m.
Proof.
  intros.
  unfold mat_mul_mat.
  rewrite height_dl_mul_dl.
  apply (mat_height A m n left).
Qed.

(** *** width_mat_mul_mat *)
(** The width of the two-dimensional list obtained by the 
    multiplication of matrices is equal to the width of the matrices. *)
Lemma width_mat_mul_mat : forall {m n p:nat} (left:@Mat A m n)
  (right:@Mat A n p),
  width (mat_mul_mat left right) p.
Proof.
  intros.
  unfold mat_mul_mat.
  apply width_dl_mul_dl. 
  apply (mat_height A p n (trans A Zero right)).
Qed.

(** ** matrix_mul *)
(** Matrix multiplication function : A × B. *)
Definition matrix_mul {m n p:nat}
  (left :@Mat A m n)( right:@Mat A n p):=
  let ll := mat_mul_mat left right in
  mkMat A m p ll (height_mat_mul_mat left right)
                 (width_mat_mul_mat left right).

(** * Definition of Multiplication Function between Matrice and constant *)

(** ** Multiplication Function of Constant and Matrix : c × A *)

(** *** c_mul_l*)
(** The multiplication of constant and list : c * l. *)
Fixpoint c_mul_l (c:A)(l:list A):=
  match l with
  | nil => nil
  | a :: t => mul c a :: c_mul_l c t
  end.

(** *** c_mul_dl *)
(** The multiplication of constant and two-dimensinal list : c * dl. *)
Fixpoint c_mul_dl (c:A)(m:list (list A)) :=
  match m with
  | nil => nil
  | a :: t => c_mul_l c a :: c_mul_dl c t 
  end.

(** *** c_mul_mat *)
(** The multiplication of constant and matrix returns two-dimensional
    list : c * M. *)
Definition c_mul_mat {m n:nat} (c:A) (ma:@Mat A m n):=
  let ma' := mat A m n ma in
  c_mul_dl c ma'.

(** *** length_c_mul_l *)
(** The length of the list obtained by the multiplication of the 
    constant and the list remains unchanged. *)
Lemma length_c_mul_l : forall (c: A) (l:list A), 
  length(c_mul_l c l) = length l.
Proof.
  intros c.
  induction l.
  - simpl. auto.
  - simpl. rewrite IHl. auto.
Qed.

(** *** height_c_mul_dl *)
(** The height of the two-dimensional list obtained by the 
    multiplication of the constant and the two-dimensional list 
    remains unchanged. *)
Lemma height_c_mul_dl : forall (c:A) (m:list(list A)),
   height(c_mul_dl c m) = height m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. rewrite IHm. auto.
Qed.

(** *** width_c_mul_dl *)
(** The width of the two-dimensional list obtained by the 
    multiplication of the constant and the matrix remains unchanged. *)
Lemma width_c_mul_dl : forall (c:A) (n:nat) (m:list(list A)),
  width m n  -> width (c_mul_dl c m) n.
Proof.
  induction n.
  induction m.
  - simpl. auto.
  - simpl. intros. inversion H. split. rewrite length_c_mul_l. auto.
    apply IHm. auto.
  - intros. induction m. auto. simpl.
    split. rewrite length_c_mul_l. inversion H. auto.
    apply IHm. inversion H. auto.
Qed.

(** *** height_c_mul_mat *)
(** The height of the two-dimensional list obtained by the 
    multiplication of the constant and the matrix remains unchanged. *)
Lemma height_c_mul_mat : forall (c:A) (m n:nat) (ma:@Mat A m n),
  height (c_mul_mat c ma) = m.
Proof.
  intros.
  unfold c_mul_mat.
  rewrite height_c_mul_dl.
  apply (mat_height A m n ma).
Qed.

(** *** width_c_mul_mat *)
(** The width of the two-dimensional list obtained by the 
    multiplication of the constant and the matrix remains unchanged. *)
Lemma width_c_mul_mat : forall (c:A) (m n:nat) (ma:@Mat A m n ) ,
  width (c_mul_mat c ma) n.
Proof.
  intros.
  unfold c_mul_mat.
  apply width_c_mul_dl.
  apply (mat_width A m n ma).
Qed.

(** ** const_mul_matrix *)
(** The multiplication of constant and matrix: c * M. *)
Definition const_mul_l{m n :nat}(c:A) (ma:@Mat A m n):=
  mkMat A m n (c_mul_mat c ma) 
    (height_c_mul_mat c m n ma) (width_c_mul_mat c m n ma).

(** ** Multiplication Function of Matrix and Constant : A × c *)

(** *** l_mul_c *)
(** The multiplication of list and constant : l * c. *)
Fixpoint l_mul_c (c:A) (l:list A) :=
  match l with
  | nil => nil
  | a :: t => mul a c :: l_mul_c c t
  end.

(** *** dl_mul_c *)
(** The multiplication of two-dimensional list and constant : dl * c.  *)
Fixpoint dl_mul_c (c:A)(m:list (list A)) :=
  match m with
  | nil => nil
  | a :: t => l_mul_c c a :: dl_mul_c c t 
  end.

(** *** mat_mul_c *)
(** The multiplication of constant and matrix returns two-dimensional
    list :  M * c. *)
Definition mat_mul_c {m n:nat}(c:A)(ma:@Mat A m n):=
  let ma' := mat A m n ma in
  dl_mul_c c ma'.

(** *** length_l_mul_c *)
(** The length of the list obtained by the multiplication of the list
    and constant remains unchanged. *)
Lemma length_l_mul_c : forall (c:A) (l:list A), 
  length(l_mul_c  c l) = length l.
Proof.
  intros c.
  induction l.
  - simpl. auto.
  - simpl. rewrite IHl. auto.
Qed.

(** *** height_dl_mul_c *)
(** The height of the two-dimensional list obtained by the 
    multiplication of two-dimensional list and constant remains 
    unchanged. *)
Lemma height_dl_mul_c : forall (c:A) (m:list(list A)),
   height(dl_mul_c c m) = length m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. rewrite IHm. auto.
Qed.

(** *** width_dl_mul_c *)
(** The width of the two-dimensional list obtained by the 
    multiplication of two-dimensional list and constant remains 
    unchanged. *)
Lemma width_dl_mul_c : forall (c:A) (n:nat) (m:list(list A)),
  width m n  -> width (dl_mul_c c m) n.
Proof.
  induction n.
  induction m.
  - simpl. auto.
  - simpl. intros. inversion H. split. rewrite length_l_mul_c. auto.
    apply IHm. auto.
  - intros. induction m. auto. simpl.
    split. rewrite length_l_mul_c. inversion H. auto.
    apply IHm. inversion H. auto.
Qed.

(** *** height_mat_mul_c *)
(** The height of the two-dimensional list obtained by the 
    multiplication of matrix and constant remains unchanged. *)
Lemma height_mat_mul_c : forall (c:A) (m n:nat) (ma:@Mat A m n),
  height (mat_mul_c c ma) = m.
Proof.
  intros.
  unfold mat_mul_c.
  rewrite height_dl_mul_c. 
  apply (mat_height A m n ma).
Qed.

(** *** width_mat_mul_c *)
(** The weight of the two-dimensional list obtained by the 
    multiplication of matrix and constant remains unchanged. *)
Lemma width_mat_mul_c : forall (c:A) (m n:nat) (ma:@Mat A m n) ,
  width (mat_mul_c c ma) n.
Proof.
  intros.
  unfold mat_mul_c.
  apply width_dl_mul_c.
  apply (mat_width A m n ma).
Qed.

(** ** const_mul_r *)
(** The multiplication of matrix and constant: M * c.*)
Definition const_mul_r {m n :nat}(c:A)(ma:@Mat A m n) :=
  mkMat A m n (mat_mul_c c ma) 
    (height_mat_mul_c c m n ma) (width_mat_mul_c c m n ma).

End Mul_def.
End Mul.


Section Extra_lemma.
Variable A:Set.
Variable Zero:A.
Variable One:A.
Variable add:A->A->A.
Variable mul:A->A->A.

(** *** l_mul_dl_nil *)
Lemma l_mul_dl_nil : forall m ma ,
  length ma = m ->
  l_mul_dl A Zero add mul nil ma = list_o A Zero m.
Proof. 
  induction m.
  - induction ma.
    + simpl. auto.
    + intros. inversion H.
  - induction ma.
    + intros. inversion H.
    + intros. simpl. f_equal. apply IHm. inversion H. auto.
Qed.

(** *** l_mul_dl_nil_list *)
Lemma l_mul_dl_nil_list : forall m a ,
  l_mul_dl A Zero add mul a (nil_list A m) = list_o A Zero m.
Proof. 
  induction m.
  - induction a.
    + simpl. auto.
    + intros. simpl. auto. 
  - induction a.
    + intros. simpl. f_equal. apply IHm. 
    + intros. simpl. f_equal. apply IHm.
Qed.

Lemma dl_mul_dl_nil_list_l : forall m n ma ,
  length ma = n ->
  dl_mul_dl A Zero add mul (nil_list A m) ma = dlist_o A Zero m n.
Proof.
  induction m.
  - simpl. auto.
  - induction n.
    + simpl. intros. rewrite l_mul_dl_nil with (m:=0). simpl.
      f_equal. apply IHm. apply H. apply H.
    + intros. simpl. rewrite l_mul_dl_nil with(m:= S n).
      simpl. f_equal. apply IHm. apply H. apply H.
Qed.

Lemma dl_mul_dl_nil_list_r : forall m n ma ,
  length ma = m -> (forall a b : A, mul a b = mul b a)->
  dl_mul_dl A Zero add mul ma (nil_list A n) = dlist_o A Zero m n.
Proof.
  induction m.
  - induction n.
    + induction ma.
      * auto. * intros. inversion H.
    + induction ma.
      * auto. * intros. inversion H.
  - induction n.
    + induction ma.
      * intros. inversion H.
      * intros. simpl. f_equal. assert(nil_list A 0 = nil).
        { auto. } rewrite <- H1. apply IHm. inversion H. auto.
        apply H0.
    + induction ma.
      * intros. inversion H.
      * intros. simpl. rewrite product'_comm. simpl.
        rewrite l_mul_dl_nil_list. f_equal. 
        assert(nil::nil_list A n = nil_list A (S n)).
        { auto. } rewrite H1. apply IHm. inversion H. auto. apply H0.
        apply H0.
Qed.

(** *** dl_mul_dl_nil *)
Lemma dl_mul_dl_nil : forall m ma ,
  length ma = m ->
  dl_mul_dl A Zero add mul ma nil = nil_list A m.
Proof.
  induction m.
  - induction ma.
    + intros. simpl. auto.
    + intros. inversion H.
  - induction ma.
    + intros.  inversion H.
    + intros. simpl. f_equal. apply IHm. inversion H. auto.
Qed.


Lemma dl_mul_dl_cons : forall m n b ma mb ,
  length ma = m -> length b = n ->
  width ma n -> width mb n-> 
  (forall a b : A, mul a b = mul b a) ->
  dl_mul_dl A Zero add mul ma (b::mb) 
  = link A (l_mul_dl A Zero add mul b ma) (dl_mul_dl A Zero add mul ma mb) .
Proof.
  induction m.
  - induction n.
    + induction b.
      * induction ma.
        simpl. auto. intros. inversion H.
      * intros. inversion H0.
    + induction b.
      * intros. inversion H0. 
      * induction ma.
        simpl. auto. intros. inversion H.
  - induction n.
    + induction b.
      * induction ma. 
        intros. inversion H. induction mb. intros. simpl. rewrite product'_comm.
        simpl. f_equal. apply IHm with(n:=0). inversion H. auto.
        auto. apply H1. auto. apply H3. apply H3. intros. simpl. 
        rewrite product'_comm. simpl. f_equal. apply IHm with(n:=0).
        inversion H. auto. auto. apply H1. apply H2. apply H3. apply H3.
      * intros. inversion H0.
    + induction b.
      * intros. inversion H0. 
      * induction ma. intros. inversion H. intros. induction a0.
        inversion H1. inversion H4. simpl. rewrite H3. rewrite product'_comm.
        f_equal. apply IHm with(n:= S n). inversion H. auto. apply H0.
        apply H1. apply H2. apply H3. apply H3.
Qed.

(** *** dlist_o_headcolumn *)
Lemma dlist_o_headcolumn: forall m n,
  headcolumn A Zero (dlist_o A Zero m n) = list_o A Zero m .
Proof.
  induction m.
  - simpl. auto.
  - induction n.
    + simpl. f_equal. apply IHm.
    + simpl. f_equal. apply IHm.
Qed.

(** *** dl_mul_dl_mul_dl *)
Lemma dl_mul_dl_headcolumn: forall n p a ma mb ,
  length a = n-> width ma n ->height mb = p-> width mb n ->
  (forall a b : A, mul a b = mul b a)->
  l_mul_dl A Zero add mul a mb 
  = headcolumn A Zero (dl_mul_dl A Zero add mul mb (a :: ma)).
Proof.
  intros.
  rewrite dl_mul_dl_cons with(m:=p)(n:=n) .
  rewrite headcolumn_link with (m:=p).
  auto. auto. rewrite length_l_mul_dl. apply H1. rewrite height_dl_mul_dl.
  apply H1. apply H1. apply H. apply H2. apply H0. apply H3.
Qed.

Lemma dl_mul_dl_tailcolumn: forall m a ma mb,
  width ma m-> length a = m -> width mb m ->
  tailcolumn A (dl_mul_dl A Zero add mul ma (a :: mb))
  = dl_mul_dl A Zero add mul ma mb.
Proof.
  induction m.
  - induction a.
    + induction ma.
      * intros. simpl. auto.
      * intros. simpl. f_equal. apply IHma. apply H. auto. apply H1.
    + intros. inversion H0.
  - induction a.
    + intros. inversion H0.
    + induction ma. 
      * simpl. auto.
      * intros. simpl. f_equal.
        apply IHma. apply H. apply H0. apply H1.
Qed.

Lemma tailcolumn_dlist_o: forall m n,
  tailcolumn A (dlist_o A Zero m (S n)) = dlist_o A Zero m n.
Proof.
  induction m.
  - simpl. auto.  
  - induction n.
    + simpl. f_equal. apply IHm.
    + simpl. f_equal. apply IHm.
Qed.


Lemma gettrans_dlist_o: forall m n,
  gettrans A Zero (dlist_o A Zero m n) n =  dlist_o A Zero n m .
Proof.
  induction m.
  - induction n.
    + auto.
    + simpl. f_equal. rewrite gettrans_nil. rewrite dlist_o_m_0. auto.
  - induction n. 
    + auto.
    + simpl. f_equal. rewrite dlist_o_headcolumn. f_equal.
      rewrite tailcolumn_dlist_o. assert(list_o A Zero n :: dlist_o A Zero m n =
      dlist_o A Zero (S m) n). { auto. } rewrite H. apply IHn.
Qed.


Lemma gettrans_headtailcolumn: forall p mb,
  width mb (S p) ->
  headcolumn A Zero mb :: gettrans A Zero (tailcolumn A mb) p = 
  gettrans A Zero mb (S p).
Proof.
  induction p.
  - intros. simpl. f_equal.
  - simpl. intros. f_equal.
Qed.



(** *** dl_mul_dl_gettrans_r *)
Lemma dl_mul_dl_gettrans_r: forall m n p ma mb,
  (forall a b : A, mul a b = mul b a)->
  height ma = m -> width ma n -> 
  height mb = n -> width mb p ->
  dl_mul_dl A Zero add mul ma (gettrans A Zero mb p)=
  gettrans A Zero (dl_mul_dl A Zero add mul (gettrans A Zero mb p) ma)m.
Proof.
  induction m.
  - induction n.
    + induction p.
      * induction ma. intros. simpl. auto. intros. inversion H0.
      * induction ma. simpl. auto. intros. inversion H0.
    + induction p.
      * induction ma. auto. intros. inversion H0. 
      * induction ma. induction mb. intros. inversion H2. intros. auto.
        intros. inversion H0.
  - induction n.
    + induction p.
      * induction ma. intros. inversion H0. intros. simpl.
        f_equal. rewrite gettrans_nil. rewrite dl_mul_dl_nil with(m:=m).
        reflexivity. inversion H0. auto.
      * induction ma. intros. inversion H0.
        intros. apply length_zero_iff_nil in H2. rewrite H2. simpl.
        rewrite product'_comm. simpl. f_equal. f_equal.
        rewrite dl_mul_dl_headcolumn with (n:=0)(p:= p)(ma:=ma).
        reflexivity. apply H1. apply H1. apply height_gettrans.
        rewrite gettrans_nil. apply width_nil_list. apply H.
        rewrite gettrans_nil. rewrite l_mul_dl_nil with(m:=m).
        rewrite dl_mul_dl_tailcolumn with(m:= 0).
        rewrite dl_mul_dl_nil_list_l with (n:=m).
        assert(nil :: nil_list A p = nil_list A (S p)).
        { auto. } rewrite H4. rewrite dl_mul_dl_nil_list_r with(m:= m).
        assert(list_o A Zero m :: dlist_o A Zero p m = dlist_o A Zero (S p)m).
        { auto. } rewrite H5. rewrite gettrans_dlist_o. auto.
        inversion H0. auto. apply H. inversion H0. auto. apply width_nil_list.
        apply H1. apply H1. inversion H0. auto. apply H.
   + induction p.
     * intros. simpl. rewrite dl_mul_dl_nil with (m:=S m).
       rewrite gettrans_nil. auto. apply H0.
     * induction ma. intros. inversion H0.
       intros. simpl. rewrite product'_comm. f_equal.
       f_equal. rewrite dl_mul_dl_headcolumn with(n:=S n)(p:= p)(ma:=ma).
       reflexivity. apply H1. apply H1. apply height_gettrans.
       apply width_gettrans. apply height_tailcolumn. apply H2.
       apply H. rewrite gettrans_headtailcolumn.
       rewrite dl_mul_dl_tailcolumn with(m:=S n).
       assert(l_mul_dl A Zero add mul (headcolumn A Zero mb) ma 
       :: dl_mul_dl A Zero add mul (gettrans A Zero (tailcolumn A mb) p) ma=
       dl_mul_dl A Zero add mul
      ((headcolumn A Zero mb::(gettrans A Zero (tailcolumn A mb) p))) ma).
      { auto. } rewrite H4. rewrite gettrans_headtailcolumn. apply IHm with (n:=S n).
      apply H. inversion H0. auto. apply H1. apply H2. apply H3. apply H3.
      apply width_gettrans. apply height_tailcolumn. apply H2. apply H1. apply H1.
      apply H3. apply H.
Qed.

(** *** dl_mul_dl_gettrans_l *)
Lemma dl_mul_dl_gettrans_l: forall m n p ma mb,
  (forall a b : A, mul a b = mul b a)->
  height ma = p -> width ma m -> 
  height mb = n -> width mb p ->
  dl_mul_dl A Zero add mul (gettrans A Zero ma m) mb=
  gettrans A Zero (dl_mul_dl A Zero add mul mb (gettrans A Zero ma m)) m .
Proof.
  intros.
  rewrite dl_mul_dl_gettrans_r with(m:=n)(n:=p).
  rewrite trans_same. reflexivity. auto.
  rewrite height_dl_mul_dl. rewrite height_gettrans. auto.
  apply width_dl_mul_dl. apply H2. apply H. apply H2. apply H3. apply H0. apply H1.
Qed.  

Lemma dl_mul_dl_nil_list: forall h w ma,
  height ma = h -> 
  dl_mul_dl A Zero add mul ma (nil_list A w) = dlist_o A Zero h w .
Proof.
  induction h. induction ma. simpl. auto.
  intros. inversion H. induction w. simpl.
  intros. rewrite dl_mul_dl_nil with(m:=S h). simpl. f_equal.
  assert(dlist_o A Zero h 0 = nil_list A h). { apply width_dlist_0. 
  apply dlist_o_height. apply dlist_o_width. } rewrite H0. auto.
  auto.
  induction ma. intros. inversion H.
  intros. simpl. f_equal. f_equal. apply product'_nil_r.
  rewrite l_mul_dl_nil_list. auto.
  assert([] :: nil_list A w = nil_list A (S w)).
  { simpl. auto. } rewrite H0. rewrite IHh.
  auto. inversion H. auto.
Qed.



Lemma l_mul_dl_app_r: forall w l dl1 dl2,
  length l = w -> 
  width dl1 w -> width dl2 w ->
  l_mul_dl A Zero add mul l (dl1 ++ dl2) =
  (l_mul_dl A Zero add mul l dl1) ++
  (l_mul_dl A Zero add mul l dl2).
Proof.
  induction w. 
  - induction l. intros. 
    rewrite l_mul_dl_nil with(m:=length(dl1)+ length(dl2)).
    rewrite l_mul_dl_nil with(m:=length(dl1)).
    rewrite l_mul_dl_nil with(m:=length(dl2)).
    rewrite list_o_app. auto. auto. auto.
    apply height_app. auto. auto. intros. inversion H. 
  - induction l. intros. inversion H.
    induction dl1. simpl. auto.
    induction dl2. intros. rewrite app_nil_r. simpl.
    rewrite app_nil_r. auto.
    intros. induction a0. inversion H0. inversion H2.
    induction a1. inversion H1. inversion H2. simpl.
    f_equal. rewrite IHdl1. f_equal. auto. apply H0.
    apply H1.
Qed.
 
Lemma dl_mul_dl_app_l: forall h1 h2 ma1 ma2 mb,
  height ma1 = h1 -> height ma2 = h2->
  dl_mul_dl A Zero add mul (ma1++ma2) mb = 
  (dl_mul_dl A Zero add mul ma1 mb) ++ 
  (dl_mul_dl A Zero add mul ma2 mb).
Proof.
  induction h1.
  induction ma1. simpl. auto. intros. inversion H.
  induction h2.
  induction ma2. intros. simpl. f_equal. rewrite ?app_nil_r.
  auto. intros. inversion H0. induction ma1. intros.
  inversion H. induction ma2. intros. inversion H0.
  induction mb. intros. simpl. f_equal.
  rewrite dl_mul_dl_nil with(m:=h1+ S h2).
  rewrite dl_mul_dl_nil with(m:= h1).
  rewrite dl_mul_dl_nil with(m:= h2).
  rewrite nil_list_app. f_equal. inversion H0. auto.
  inversion H. auto. apply height_app. inversion H.
  auto. apply H0. intros. simpl.
  f_equal. rewrite IHh1 with(h2:=S h2).
  f_equal. inversion H. auto. auto.
Qed. 

End Extra_lemma.

Lemma dl_mul_dl_compat: forall A Zero add mul m n p 
  ma mb mc md,
  height ma = m -> height mc = m ->
  height mb = n -> height md = n ->
  width ma n-> width mc n ->
  width mb p -> width md p ->
  ma = mc -> mb  = md ->
  dl_mul_dl A Zero add mul ma (gettrans A Zero mb p) =
  dl_mul_dl A Zero add mul mc (gettrans A Zero md p).
Proof.
  induction m.
  - induction ma,mc. intros. simpl. auto.
    intros. inversion H0. intros. inversion H.
    intros. inversion H.
  - induction n. 
    + induction mb,md. intros. rewrite gettrans_nil.
      rewrite ?dl_mul_dl_nil_list with(h:=S m). auto.
      auto. auto. intros. inversion H2. intros. inversion H1.
      intros. inversion H1. 
    + induction p. 
      * intros. simpl. rewrite ?dl_mul_dl_nil with(m:=S m).
        auto. auto. auto.
      * induction ma. intros. inversion H.
        induction mb. intros. inversion H1.
        induction mc. intros. inversion H0.
        induction md. intros. inversion H2.
        intros. simpl. f_equal. f_equal.
        inversion H7. inversion H8. auto.
        inversion H7. inversion H8. auto.
        inversion H7. inversion H8. auto.
Qed.

Lemma matrix_mul_compat : 
  forall (A:Set) Zero add mul m n p, 
     forall x x' : (@Mat A m n), @M_eq A m n x x' ->
     forall y y' : (@Mat A n p), @M_eq A n p y y' ->
         @M_eq A m p 
    (matrix_mul A Zero add mul x  y) 
    (matrix_mul A Zero add mul x' y').
Proof.
  induction x,x',y,y'. unfold M_eq,matrix_mul,mat_mul_mat.
  simpl. unfold M_eq in H. simpl in H. intros. 
  apply dl_mul_dl_compat with(m:= m)(n:= n). auto. auto.
  auto. auto. auto. auto. auto. auto. auto. auto.
Qed.

Add Parametric Morphism {A:Set}{Zero}add mul {m n p:nat}: (matrix_mul A Zero add mul)
  with signature (@M_eq A m n) ==> (@M_eq A n p) ==> (@M_eq A m p) 
  as mat_mul_mor.
Proof.
  exact (matrix_mul_compat A Zero add mul m n p).
Qed.
